Nuprl Lemma : data_wf
11,40
postcript
pdf
T
:(Id
Type). data(
T
)
Type
latex
Definitions
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
data(
T
)
Lemmas
Id
wf
origin
T:(Id
Type). data(T) 
Type T:(IdType). data(T) Type Tx:A. B(x)